<html>
<head><meta charset="utf-8"><title>implied-bounds-flaw · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html">implied-bounds-flaw</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="154759918"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154759918" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154759918">(Jan 09 2019 at 21:39)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> For a moment I thought the world was tearing apart, but that's ok</p>



<a name="154759924"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154759924" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154759924">(Jan 09 2019 at 21:40)</a>:</h4>
<p>we just overlooked something with implied bounds</p>



<a name="154760001"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760001" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760001">(Jan 09 2019 at 21:40)</a>:</h4>
<p>I mean I overlooked something, with my "optimization" that if you have say a function <code>fn foo&lt;T: Foo&gt;()</code>, and you call it with e.g. <code>foo::&lt;SomeType&gt;</code>, the caller only has to prove <code>Implemented(SomeType: Foo)</code> while the function can rely on <code>FromEnv(T: Foo)</code></p>



<a name="154760010"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760010" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760010">(Jan 09 2019 at 21:40)</a>:</h4>
<p>well guess what, this optimization is wrong</p>



<a name="154760028"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760028" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760028">(Jan 09 2019 at 21:41)</a>:</h4>
<p>the caller should be proving the full <code>WellFormed(SomeType: Foo)</code></p>



<a name="154760044"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760044" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760044">(Jan 09 2019 at 21:41)</a>:</h4>
<p>trivial example of why this optimization is wrong:</p>
<div class="codehilite"><pre><span></span><span class="cp">#![feature(trivial_bounds)]</span><span class="w"></span>

<span class="k">trait</span><span class="w"> </span><span class="n">Bar</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">fn</span> <span class="nf">foo</span><span class="p">();</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
<span class="k">trait</span><span class="w"> </span><span class="n">Foo</span>: <span class="nc">Bar</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="c1">// `WF(S) :- Implemented(S: Foo).` ok</span>
<span class="c1">// and the implied bound:</span>
<span class="c1">// `FromEnv(S: Foo) :- FromEnv(S)`</span>
<span class="k">struct</span> <span class="nc">S</span><span class="w"> </span><span class="k">where</span><span class="w"> </span><span class="n">S</span>: <span class="nc">Foo</span><span class="p">;</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="c1">// We have `FromEnv(S)` which implies `Implemented(S: Foo)` and `Implemented(S: Bar)`,</span>
<span class="c1">// so we can prove `WellFormed(S: Foo)`.</span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">bar</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nc">Bar</span><span class="o">&gt;</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// Well `T = S` here and we never wrote a `Bar` impl for `S` actually.</span>
<span class="w">    </span><span class="n">T</span>::<span class="n">foo</span><span class="p">();</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&gt;</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// I can rely on `FromEnv(T: Foo)`, hence I can prove `Implemented(T: Bar)`.</span>
<span class="w">    </span><span class="n">bar</span>::<span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">main</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// Ok I can prove `Implemented(S: Foo)` because of the impl</span>
<span class="w">    </span><span class="n">foo</span>::<span class="o">&lt;</span><span class="n">S</span><span class="o">&gt;</span><span class="p">()</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>



<a name="154760272"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760272" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760272">(Jan 09 2019 at 21:45)</a>:</h4>
<p>makes sense</p>



<a name="154760285"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760285" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760285">(Jan 09 2019 at 21:45)</a>:</h4>
<p>amazing how subtle this can be :)</p>



<a name="154760287"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760287" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760287">(Jan 09 2019 at 21:45)</a>:</h4>
<p>I guess we won't lose a lot without this optimization thanks to caching</p>



<a name="154760288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760288">(Jan 09 2019 at 21:45)</a>:</h4>
<p>I don't even remember this optimization, I have to admit</p>



<a name="154760295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/154760295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#154760295">(Jan 09 2019 at 21:45)</a>:</h4>
<p>yep</p>



<a name="155111465"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/155111465" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#155111465">(Jan 14 2019 at 19:54)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> should I be putting this on some list of "things we need to follow up on"?</p>



<a name="155111510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/155111510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#155111510">(Jan 14 2019 at 19:55)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yes</p>



<a name="156721531"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/implied-bounds-flaw/near/156721531" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/implied-bounds-flaw.html#156721531">(Jan 23 2019 at 20:20)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span></p>
<blockquote>
<p>We can see that we have this asymmetry between well-formedness check, which only verifies that the direct superbounds hold, and implied bounds which gives access to all bounds transitively implied by the where clauses. In that case this is ok because as we said, we don't use FromEnv(Type&lt;...&gt;) to deduce other FromEnv(OtherType&lt;...&gt;) things, nor do we use FromEnv(Type: Trait) to deduce FromEnv(OtherType&lt;...&gt;) things. So in that sense type definitions are "less recursive" than traits, and we saw in a previous subsection that it was the combination of asymmetry and recursive trait / impls that led to unsoundness. As such, the WellFormed(Type&lt;...&gt;) predicate does not need to be co-inductive.</p>
</blockquote>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>